# -*- mode: org; fill-column: 80; -*-
#+TITLE: Lambda Calculus
#+AUTHOR: Zelphir Kaltstahl
#+STARTUP: content indent align inlineimages hideblocks entitiesplain nologdone nologreschedule nologredeadline nologrefile
#+KEYWORDS: lambda calculus notes
#+TODO: TODO INPROGRESS | DONE CANCELLED
#+DATE: [2022-10-14 Fr]
#+LANGUAGE: en
#+PRIORITIES: A E E
#+OPTIONS: ^:{}
#+OPTIONS: H:10
#+OPTIONS: toc:2
#+OPTIONS: tags:nil
#+OPTIONS: tasks:nil
#+OPTIONS: H:6
#+OPTIONS: p:nil
#+OPTIONS: pri:nil
#+OPTIONS: prop:nil
#+OPTIONS: todo:nil
#+OPTIONS: stat:nil
#+OPTIONS: |:t
#+OPTIONS: inline:nil

* Lambda
:PROPERTIES:
:CUSTOM_ID: lambda
:END:

** Encoding booleans in lambda calculus
:PROPERTIES:
:CUSTOM_ID: encoding-booleans
:END:

Booleans can be seen as making a choice between 2 alternatives. Imagine an ~if~
expression in any programming language. If checks a condition, which results in
a boolean and depending on that boolean, it makes a choice between the things to
do, if the boolean is ~true~ and the alternative things to do, if the boolean is
~false~. So in principle all the boolean needs to do is allowing to make a
choice between 2 alternatives.

If booleans have this property, then it will be possible to design other boolean
functions like ~not~ on top of them. As long as they return ~true~ or ~false~
again, they create a perfect abstraction layer on top of the representation of
booleans. As long as booleans are the result, no other part of the program needs
to know anything more specific about them. How they are represented is merely an
implementation detail.

One way to encode booleans is the following:

*** true
:PROPERTIES:
:CUSTOM_ID: encoding-booleans-true
:END:

~true~ is encoded by choosing the first of 2 arguments:

#+begin_src lambda
λx.λy.x
#+end_src

*** false
:PROPERTIES:
:CUSTOM_ID: encoding-booleans-false
:END:

~false~ is encoded by choosing the second of 2 arguments:

#+begin_src lambda
λx.λy.y
#+end_src

*** Implementing another boolean function: ~not~
:PROPERTIES:
:CUSTOM_ID: encoding-booleans-other
:END:

~not~ applies the choice of ~b~ to ~false~ and ~true~:

#+begin_src lambda
  λb.b false true
= λb.b (λx.λy.y) (λx.λy.x)
= NOT

  NOT true
= (λb.b (λx.λy.y) (λx.λy.x)) true
= (λb.b (λx.λy.y) (λx.λy.x)) (λx.λy.x)
= (λx.λy.x) (λx.λy.y) (λx.λy.x)
= λx is (λx.λy.y) . λy is (λx.λy.x) . x
= (λx.λy.y)
= λx.λy.y
= false
#+end_src

In the case of ~b~ being ~false~, this will result in the second argument being
chose, which is ~true~. In the case of ~b~ being ~true~, the first argument will
be chosen, which is ~false~. ~not~ returns our representation of ~true~ and
~false~!

** Function application ("β-reduction")
:PROPERTIES:
:CUSTOM_ID: function-application
:END:

Function application is written by putting a function and its argument next to
each other (juxtapositioning). For example:

#+begin_src lambda
λa.a b
#+end_src

In the expression above the function ~λa.a~, the identity function, is applied
to its argument ~b~.

** Function composition
:PROPERTIES:
:CUSTOM_ID: function-composition
:END:

Function composition means taking 2 or more functions and building a new
function, which applies them in an appropriate order. The newly built function
is the composed function.

Function composition works by taking functions as arguments and then
juxtapositioning them in the function body:

#+begin_src lambda
compose := λf.λg.λx.f (g x)
#+end_src
